SizeUnsolvedConstraintsInTypeSignature.agda:21,33-39
(↑ i) !=< i of type Size
when checking that the expression one2 i has type Nat (↑ (↑ i))
